COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M1BASL30\M2BASB30\M3NGR25\M4NGR20\F2\CSTANFORD UNIVERSITY
C00004 ENDMK
C⊗;
\\M1BASL30;\M2BASB30;\M3NGR25;\M4NGR20;\F2\CSTANFORD UNIVERSITY
\F3\CSTANFORD, CALIFORNIA 94305
\F4COMPUTER SCIENCE DEPARTMENT\←L\-R\/'7;\+R\→.\→S   Telephone:
\←S\→.415-321-2300
\F1\CFeb 6,1974









Dr. Patrick Suppes
Institute for Mathematical Studies in the Social Sciences
Ventura Hall

Dear Dr. Suppes:

\JDr. Luckham suggested that your group might be intereseted in receiving
copies of our documentation.  The enclosed SAILON describes a simple
version of the on-line theorem prover.

The  proof-guidance and -checking commands represent a minimal usable
set. However they have been used successfully to discover non-trivial
proofs. Major program revisions, stressing techniques for describing intuitive proof
strategies, are forthcoming.\.

\←L\→S\←R\-L\/'2;\+L\→L

Yours sincerely,



John R. Allen
Research Associate
Computer Science Dept
Artificial Intelligence Labs

\←S\→L
JRA:pdp10